$\forall$$R$:Realizer. R{-}base{-}domain($R$) $\in$ $n$:$\mathbb{Z}\times$base{-}domain{-}type($n$)